Nuprl Lemma : es-interface-val-co-restrict 11,40
A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))), e:E.
((e  (I|p)))  ((I|p)(e) = I(e)  A) 
latex

Definitionst  T, P  Q, x:A. B(x), x. t(x), E, f(a), x(s), Type, ES, Top, left + right, x:AB(x), , Dec(P), Void, x:A.B(x), S  T, x.A(x), suptype(S; T), p-co-restrict(f;p), can-apply(f;x), b, X(e), (I|p), e  X, AbsInterface(A)
Lemmasassert wf, can-apply wf, p-co-restrict wf, decidable wf, es-E wf, top wf, event system wf, do-apply-p-co-restrict

origin